(declare-fun a () String)
(declare-fun b () Int)
(assert (<= b 72))
(assert (= (int.to.str b) (str.++ "0" a)))
(assert (distinct a ""))
(check-sat)
(declare-fun a () String)
(declare-fun b () Int)
(assert (<= b 72))
(assert (= (int.to.str b) (str.++ "0" a)))
(assert (distinct a ""))
(check-sat)
